ISSN 1884-0760
GRACE TECHNICAL REPORTS
“Putback” is the Essence of Bidirectional
Programming
Sebastian Fischer Zhenjiang Hu Hugo Pacheco
GRACE-TR 2012-08 December 2012
CENTER FOR GLOBAL RESEARCH IN
Bidirectional transformations, programs with a forward and a backward transformation that maintain consistency between input and output, are routinely written in ways that do not let programmers specify their behavior completely. Several bidirectional programming languages exist to aid program-mers in writing bidirectional transformations with increased maintainability but decreased expressiveness.
Such languages allow programmers to write bidirectional transformations as one program for both directions, which is easier to maintain than separate programs for each direction. However, the maintainability provided by exist-ing bidirectional languages comes at the cost of expressiveness because the ambiguity of synchronization is solved by default strategies which are hidden from programmers. The programmers’ inability to influence synchronization strategies has led to the proposal of a vast number of approaches that consider tailor-made synchronization strategies for particular applications.
In this paper, we argue that such ambiguity is essential for bidirectional transformation and advocate that the synchronization strategy should not be hidden from programmers but considered from the start. We propose a novel approach to specifying so called well-behaved bidirectional programs by their backward transformations, capable of expressing all aspects of a bidirectional transformation completely, while retaining maintainability.
“Putback” is the Essence of Bidirectional
Programming
Sebastian Fischer Zhenjiang Hu Hugo Pacheco
December 2012
The further backward you can look, the further forward you can see.
– Winston Churchill
1 Introduction
Bidirectional transformation (BX for short) [Czarnecki et al., 2009, Hu et al., 2011], originated from theview updating mechanism in the database community [Bancilhon and Spyratos, 1981, Dayal and Bernstein, 1982, Gottlob et al., 1988], has been recently at-tracting a lot of attention from researchers in the communities of programming languages and software engineering since the pioneering work on a combinatorial language for bidi-rectional tree transformation [Foster et al., 2007]. Bidibidi-rectional transformation provides a novel mechanism for synchronizing and maintaining the consistency of information between input and output, and has seen many interesting applications, including the synchronization of replicated data in different formats [Foster et al., 2007], presentation-oriented structured document development [Hu et al., 2008], interactive user interface design [Meertens, 1998] or coupled software transformation [L¨ammel, 2004].
1.1 Bidirectional Transformation (BX)
A bidirectional transformationconsists of a pair of transformations: theforward transfor-mation is used to produce a target view from a source, while thebackwardtransformation is used to “put back” modifications on the view to the source. To allow the forward trans-formation to discard intrans-formation when producing a view, the backward transtrans-formation is supplied the original source in addition to the updated view. This situation is depicted in Figure 1 where, as is customary, the forward transformation is calledget (also know as view function) and the backward transformation is calledput (shorthand for “putback”).
Figure 1: Forward and Backward Directions in Bidirectional Transformations
function putFirst that updates the first component and retains the second component from the original pair.
getFirst (x,y) =x putFirst (x,y)z = (z,y)
Not every combination of get and put functions forms a reasonable bidirectional transformation. The definitions need to fit together in the sense that one constitutes the opposite direction of the other. Put formally, theget andput functions of a bidirectional transformation should bewell-behavedin the sense that they satisfy the followingGetPut
and PutGetlaws.
put s (get s) =s GetPut
get (put s v) =v PutGet
The GetPut property requires that not changing the view shall be reflected as not
changing the source, while thePutGet property requires all changes in the view to be
completely reflected to the source so that the changed view can be computed again by applying the forward transformation to the changed source.
1.2 Bidirectional Programming
Bidirectional programming is to develop well-behaved bidirectional transformations in order to solve various synchronization problems.
is a maintenance problem if a modification to one of the transformations requires a redefinition of the other transformation as well as a new proof of the laws.
To ease bidirectional programming and to enable maintainable bidirectional program-ming, it is preferable to write just a single program that can denote both transformations, which has motivated the following two methods:
• Bidirectionalization of Forward Transformation. This is to allow users to write the forward transformation in a familiar (unidirectional) programming language, and derive a suitable backward transformation throughbidirectionalization techniques [Keller, 1986, Larson and Sheth, 1991, Xiong et al., 2007, Matsuda et al., 2007, Voigtl¨ander, 2009, Hidaka et al., 2010].
• Design of Domain-specific BX Languages. This is to instruct users to write a program in a particular bidirectional programming language [Foster et al., 2007, Bohannon et al., 2006, 2008, Pacheco and Cunha, 2010, Hofmann et al., 2011, 2012, Pacheco et al., 2012], from which both transformations can be derived.
What both methods have in common is that one writes a forward transformation in a unidirectional language or a domain-specific BX language, and a corresponding good backward transformation can be automatically derived, which makes bidirectional programming easy and maintainable. Despite these advantages, there is an impractical assumption that
for a forward transformationget, it is sufficient to derive a “suitable” put
that can be combined to form a well-behaved bidirectional transformation.
In general a get function may not be injective, so there may exist many possible put
functions that can be combined withget to form a bidirectional transformation. Moreover, the most “suitable” or “best” backward transformation may be hard to find and to justify. There is no clear consensus on the best requirements even for well-studied domains [Buneman et al., 2008].
To understand the inherent ambiguity in possible “putback” functions, consider, as an example, the following forward transformation.1
getEvens:: [Int]→[Int]
getEvens ns =filter even ns
It returns those elements of a list of numbers which are even.
evens [2,3,5,6] = [2,6]
What is its corresponding put? If 6 is eliminated from the result, leaving the view list [2], there are many well-behaved ways of putting back this elimination to the source. For
1
We use Haskell syntax for our examples as we discuss further in Section 3.1. Thefilter function is
predefined and selects all elements from a list that satisfy the given predicate – in this caseeven,
example, we could delete the number 6 from the source [2,3,5,6] to obtain the updated source [2,3,5] or change 6 to n obtaining [2,3,5,n] wheren is an arbitrary odd number. Keller [1986] argues that many of these “putback” functions are incomparable, and that there is no reasonable approach to say which is the best.
It is this unavoidable ambiguity ofput that makes bidirectional programming difficult to be used in practice due to possibly unpredictable behaviors, and that has led to the boom of current bidirectional frameworks that propose to answer the needs of particular bidirectional applications [Czarnecki et al., 2009, Hu et al., 2011].
1.3 Putback-based Bidirectional Programming
So far, bidirectional programming has been focused on writing the forward transformation (or a bidirectional program that resembles writing the forward transformation), and then trying to derive a suitable (but less predictable) backward transformation that embodies a specific way to solve the ambiguity of update translation (i.e., an update strategy) [Keller, 1986, Barbosa et al., 2010, Pacheco et al., 2012]. Nevertheless, whatever update strategy is given, it does not resolve the ambiguity problem because there is in general no best update strategy [Buneman et al., 2008].
In this paper, we argue that the update strategy should be considered from the start, and propose a novel putback-based approach to bidirectional programming: writing put
and derivingget (i.e., specifying the intended backward transformation that best suits particular purposes, and deriving the forward transformation.) The new approach attains the advantages of writing a single program to specify a bidirectional transformation to enable easy maintenance. It also enjoys an important feature that, in sharp contrast to bidirectional programming based on get where get is not sufficient to determine put, bidirectional programming based on put has the potential to describe all intentions of bidirectional transformations, since there is only one get that can be combined with a given put to form a well-behaved bidirectional transformation.
There are two major difficulties in constructing a framework for putback-based bidi-rectional programming. One is to clarify sufficient and necessary conditions on the put
function such that it can be used to describe all intentions of a well-behaved bidirectional transformation while guaranteeing existence and uniqueness of the corresponding get
function. The other difficulty is how to automatically derive the unique get from put in practice. Our main technical contributions can be summarized as follows.
• We clarify necessary conditions on putback functions of well-behaved bidirectional transformations in Section 3 and use these conditions to characterize different classes of BXs in Section 4.
• In the same section, we formally prove that for a given put function that satisfies the identified necessary conditions the correspondingget function is unique in each considered class of BXs. Hence, theget function is redundant and can be derived automatically, retaining maintainability and full control over the update strategy.
• In Section 5, we describe a prototype implementation of deriving get from put
Figure 2: TheGetPutlaw Figure 3: The PutGetlaw
demonstrate how to program in putback style using programs that implement different update strategies for transformations resembling database queries.
We begin in Section 2 by discussing the considered classes of BXs more formally and provide corresponding intuitions using examples that we also use to show the ambiguity of backward transformations for given forward transformations. We discuss related work in Section 6 and provide our conclusions together with possibilities for future work in Section 7.
2 Classes of Bidirectional Transformations
In this section we review different classes of bidirectional transformations, discussing their laws both equationally and intuitively. Example transformations in this section are minimalistic to highlight the essential differences between different classes of BXs.
2.1 Well-behaved BXs
Foster et al. [2007] call bidirectional transformations that satisfy the GetPut and PutGetlawswell-behaved.
Definition 2.1 (GetPut law). The GetPut law describes a property of calling the
forward function get before the backward function put.
put s (get s) =s
It is depicted in Figure 2.
Definition 2.2 (PutGet law). The PutGet law describes a property of calling the
backward function put before the forward function get.
get (put s v) =v
It is depicted in Figure 3.
When passing a source obtained by put to get then get should yield the same view that was passed to put. This property captures the intuition that view updates are reflected in the source type by put and can be observed by get.
The bidirectional transformation defined in Example 1.1 is well-behaved because it satisfies the GetPut and PutGet laws. To verify the GetPut law, consider the
following equations.
putFirst (x,y) (getFirst (x,y)) = { definition ofgetFirst }
putFirst (x,y)x
= { definition ofputFirst }
(x,y)
So, indeed, when we update the first component of a pair with its own first component, the pair does not change.
To verify the PutGetlaw, consider the equations below.
getFirst (putFirst (x,y)z) = { definition ofputFirst }
getFirst (z,y)
= { definition ofgetFirst }
z
So, indeed, if we query the first component of a pair with an updated first component, we get back the value used for updating.
Example 2.3 (Change counter). As another example for a well-behaved bidirectional transformation, consider the combination of getFirst with the following backward function.
putFirstCount (n,c)m =if n=I m then(m,c)else(m,c+ 1)
This function increments the second component of a pair whenever we change its first component.
To verify the GetPutlaw, we can check the following equations.
putFirstCount (n,c) (getFirst (n,c)) = { definition ofgetFirst }
putFirstCount (n,c)n
Figure 4: The PutPutlaw
if n=I n then(n,c)else(n,c+ 1) = { reduction tothen branch}
(n,c)
Because we do not change the first component during the update, the counter is not incremented.
To verify the PutGetlaw, we can proceed as follows.
getFirst (putFirstCount (n,c)m) = { definition ofputFirstCount }
getFirst (if n=I m then(m,c)else(m,c+ 1)) = { reduction ofgetFirst in both branches }
m
Regardless of whether the counter is incremented, the first component of an updated pair is the value used for updating.
2.2 Very well-behaved BXs
Foster et al. [2007] call well-behaved bidirectional transformations that also satisfy the
PutPutlaw very well-behaved.
Definition 2.4 (PutPut law). The PutPut law describes a property of calling the
backward function put twice with different views.
put (put s v′)v =put s v PutPut
It is depicted in Figure 4.
The bidirectional transformation defined in Example 1.1 is very well-behaved, as can be verified by the following equations.
putFirst (putFirst (x,y)z1)z2
= { definition ofputFirst }
putFirst (z1,y)z2
= { definition ofputFirst }
(z2,y)
= { definition ofputFirst }
putFirst (x,y)z2
The first update (using the value z1) does not influence the second update (using z2)
because updates completely overwrite the effect of previous updates.
The bidirectional transformation defined in Example 2.3 is not very well-behaved because the PutPutlaw is violated if two updates in a row change the first component
of the pair more often than the second update alone.
putFirstCount (putFirstCount (42,0) 43) 42 = { definition ofputFirstCount }
putFirstCount (43,1) 42
= { definition ofputFirstCount }
(42,2)
6
= (42,0)
= { definition ofputFirstCount }
putFirstCount (42,0) 42
Different updates are not independent because their effect on the counter cannot be overwritten.
Example 2.5 (Maintaining difference). As a second example of a bidirectional transfor-mation that is very well-behaved consider the function getFirst together with the following backward function that maintains the original difference of the components of a pair when updating the first component.
putFirstDiff (x,y)z = (z,z+y−x)
When updating the first component, the second is also changed such that the difference between the components remains the same. Here are some example calls to clarify this behavior.
putFirstDiff (1,2) 3 = (3,3 + 2−1) = (3,4)
putFirstDiff (1,1) 1 = (1,1 + 1−1) = (1,1)
The following equations show that the GetPut,PutGet, andPutPut laws hold,
respectively, for the bidirectional transformation defined in Example 2.5.
putFirstDiff (x,y) (getFirst (x,y)) = { definition ofgetFirst }
putFirstDiff (x,y)x
= { definition ofputFirstDiff }
(x,x+y−x)
= { associativity and inverse of addition}
(x,y)
getFirst (putFirstDiff (x,y)z) = { definition ofputFirstDiff }
getFirst (z,z +y−x) = { definition ofgetFirst }
z
putFirstDiff (putFirstDiff (x,y)z1)z2
= { definition ofputFirstDiff }
putFirstDiff (z1, z1+y−x)z2
= { definition ofputFirstDiff }
(z2, z2+z1+y−x−z1)
= { associativity and inverse of addition}
(z2, z2+y−x)
= { definition ofputFirstDiff }
putFirstDiff (x,y)z2
Example 2.5 follows a general pattern to construct very well-behaved bidirectional transformations by maintaining a constant complement [Bancilhon and Spyratos, 1981] of the view in invocations of the put function. In fact, Foster et al. [2007] prove that view updating under constant complement captures every very well-behaved BX.
2.3 Bijective BXs
Foster et al. [2007] call bidirectional transformations that satisfy the StrongGetPut
law in addition to thePutGetlaw bijective.
Definition 2.6(StrongGetPutlaw). The StrongGetPutlaw is a stronger version
of theGetPut law for well-behaved bidirectional transformations.
put s′ (get s) =s StrongGetPut
When put is called on the result of get it should yield the same source that was given to get initially, regardless of what source is used for the update. Together with the PutGet
law (see Definition 2.2) the StrongGetPut law captures the intuition that there is a
The bidirectional transformation defined in Example 1.1 is not bijective because there is no one-to-one correspondence between pairs and their first components. To verify that theStrongGetPutlaw is violated, consider the following inequality.
putFirst (1,2) (getFirst (3,4)) = { definition ofgetFirst }
putFirst (1,2) 3
= { definition ofputFirst }
(3,2)
6
= (3,4)
Unlike (very) well-behaved BXs, bijective BXs do not allow to discard information when computing a view from a source. Examples 2.3 and 2.5 also do not define bijective bidirectional transformations because they use the same forward function as Example 1.1 which discards information.
3 Preliminary observations on putback functions
We now introduce notation and review mathematical concepts that play a role when we characterize the different classes of BXs in Section 4. While doing so, we observe necessary conditions onput functions implied by laws for bidirectional transformations.
3.1 Currying, point-free style, and infix operator sections
We denote function application by juxtaposition (as in the functional programming language Haskell [Marlow (editor), 2010]). For example, the application of a functionget
to a source arguments is written as follows.
get s
We write functions with multiple arguments in so-called curried style, i.e., instead of taking (a tuple of) multiple arguments directly, multi-argument functions take one argument and yield a function for the remaining arguments. As is conventional, function application associates to the left and, hence, the application of a functionput to a source arguments and a view argumentv is written as follows.
put s v = (put s)v
The higher-order functionscurry anduncurrytranslate between the curried and uncurried versions of a function.
curry f x y =f (x,y)
uncurry f (x,y) =f x y
For example, we can obtain the uncurried version of a put function by callinguncurry
uncurry put (s,v) =put s v
Sometimes, we give type annotations for functions, again in Haskell notation. If sources have typeS and views are of type V then curried and uncurriedput functions have the following types, respectively.
put ::S →(V →S)
uncurry put:: (S,V)→S
As is conventional, the function-type constructor associates to the right, so the type
S →(V →S) can be written S →V →S, for short.
We write id for the identity function on arbitrary types. To highlight a specific argument (and result) type of id we sometimes write it as a subscript, such as idS for
the identity function on a type S.
We write a dot to denote function composition. For example, the composition of a partially appliedput function with aget function, applyingget to the result ofput s, is written as follows.
get ·put s =λv →get (put s v)
Lambda abstractions, like the one above, define anonymous functions.
Binary functions, such as put, can be enclosed in backquotes to use them as infix operators. Furthermore, partial applications of infix operators can be formed for the first and second argument using parenthesized infix operator sections where only the left (i.e., first) or right (i.e., second) argument is provided. The following examples, demonstrate the use of such notation.
s‘put‘v =put s v
(s‘put‘) =λv →put s v =put s
(‘put‘v) =λs →put s v
Proposition 3.1 (Point-free laws for BXs). We can now rephrase some of the laws for bidirectional transformations reviewed in Section 2 in so-called point-free style, i.e., without mentioning some arguments of functions.
1. The PutGet law (cf. Definition 2.2) states the following equation for all sources
s.
get·put s =id
2. The PutPut law (cf. Definition 2.4) states the following equation for all views v
and v′.
3. The StrongGetPut law (cf. Definition 2.6) states the following equation for all
sources s.
put s·get =id
Reformulating laws in point-free style will help identify necessary conditions on putback functions using standard mathematical terminology.
3.2 Mathematical propositions
This subsection recalls basic mathematical concepts used subsequently and relates them to the previously introduced notation.
Definition 3.2 (Injectivity and left inverse). A function f ::A→B is injective if and only if there is a function g::B →A such that g·f =idA. In this case, g is called left
inverse of f .
Intuitively, an injective function maps different arguments to different results. As a consequence, the result type is “at least as big as” the argument type.
Definition 3.3 (Surjectivity and right inverse). A function f ::A→B is surjective on
B if and only if there is a function g ::B →A such that f ·g =idB. In this case, g is
called right inverse of f .
Intuitively, a surjective function yields every value in its result type for some argument. As a consequence, the argument type is “at least as big as” the result type.
Proposition 3.4 (Injectivity and Surjectivity in BXs). Certain laws for bidirectional transformations impose injectivity and surjectivity requirements on bidirectional transfor-mations.
1. The PutGetlaw (cf. Proposition 3.1) implies that get is surjective on the view
type V and “put s” is injective for all sources s. If the PutGet law holds then,
for all sources s, get is a left inverse of “put s” and “put s” is a right inverse of get.
2. The StrongGetPut law (cf. Proposition 3.1) implies that get is injective and
“put s” is surjective on the source type S for all sources s. If the StrongGetPut
law holds then, for all sources s, get is a right inverse of “put s” and “put s” is a left inverse of get.
Intuitively, a bijective function defines a one-to-one correspondence between its argu-ment and result type. As a consequence, both have the same cardinality.
Proposition 3.4 justifies why bidirectional transformations that satisfy both the Put-Get as well as theStrongGetPut law are called bijective, because in this case get
is bijective and put s is its inverse for all sources s. This shows that put functions in bijective bidirectional transformations can ignore their source argument, such that they trivially satisfy the PutPut law (cf. Definition 2.4). Therefore, every bijective
bidirectional transformation is also very well behaved.
It is worth considering the differences between the properties defined in Definitions 3.2– 3.5 for multi-argument functions in curried and uncurried style. For example, for a given
put function we can distinguish the following notions of injectivity.
1. put is injective
2. put s is injective for all source valuess
3. uncurry put is injective
We can build an intuition for the differences between these properties by considering the cardinalities of source and view types, say|S|and |V|respectively.
The cardinality of the argument type S of put is |S|and the cardinality of its result typeV →S is |S||V|. Therefore, it is easy to give an injectiveput function. In fact, the
constantput function defined as follows is an example.
put s v =s
On the other hand, the argument type (S,V) ofuncurry put has cardinality |S| · |V|
and its result typeS has cardinality|S|. So, for finite source and view types with |V|>1 there is noput function such thatuncurry put is injective.
Property 2 lies in-between properties 1 and 3. For source types that are “at least as big as” the view type, there areput functions that satisfy property 2. The constantput
function, however, is a counter example because all views are mapped to the same source. We can make similar observations for surjectivity instead of injectivity of multi-argument functions.
Proposition 3.6 (Surjectivity of uncurry put). The GetPutlaw (cf. Definition 2.1)
implies that “uncurry put” is surjective on the source type.
Proof. If the GetPut law holds then the function “pr
= λs → (s,get s)” is a right inverse of “uncurry put”:
uncurry put(pr s) = { definition ofpr
}
uncurry put(s,get s) = { definition ofuncurry }
= { GetPutlaw}
s
Our final mathematical concept that turns out helpful for characterizing the different classes of BXs introduced in Section 2 is idempotence.
Definition 3.7(Idempotence). A function f::A→A is called idempotentif the following equation holds.
f ·f =f
This notion is useful to observe that well-behaved BXs satisfy a weaker version of the
PutPutlaw (cf. Proposition 3.1).
Proposition 3.8 (Idempotence of (‘put‘v)). In a well-behaved bidirectional transfor-mation, i.e., which satisfies the GetPut and PutGet laws, the function (‘put‘v) is
idempotent for all views v . This idempotence requirement can also be expressed as the following equation, called PutTwice law [Foster, 2009].
put (put s v)v =put s v PutTwice
Proof. The following equations use thePutGetandGetPutlaws to derive the claimed
idempotence requirement.
((‘put‘v)·(‘put‘v))s
= { function composition}
(s‘put‘v) ‘put‘v
= { prefix notation}
put(put s v)v
= { PutGetlaw}
put(put s v) (get (put s v)) = { GetPutlaw}
put s v
= { infix operator section}
(‘put‘v)s
ThePutPutlaw is stronger than idempotence of (‘put‘v) because it requires a similar
equation for compositions ofputapplied to different viewsv andv′ instead of compositions
of put applied to the same view. Example 2.3 shows that the PutPutlaw is stronger
4 Characterizing BXs in terms of the putback function
We now characterize different classes of BXs introduced in Section 2 based on necessary conditions observed in Section 3. From this characterization we will be able to identify exactly, for each introduced class of BXs, which part of the definition of a bidirectional transformation is redundant due to the corresponding laws.
As a preliminary observation, note that for bijective BXs the put function is uniquely determined by theget function and vice-versa. We can define
put s =get−1
for all sourcess to derive a uniqueput from get. We can also define
get s = (put s)−1 s
to derive a uniqueget from put.
For (very) well-behaved BXs theget function does not give rise to a uniqueputfunction. Examples 1.1 and 2.5 are two different very well-behaved BXs with the sameput function. Hence, (very) well-behaved BXs cannot be specified completely by only providing aget
function.
In the remainder of this section, we show that (very) well-behaved BXs can be specified completely by giving their put function. No additional conditions on put functions are required apart from necessary conditions observed in Section 3.
4.1 Characterizing well-behaved BXs
Our first theorem shows that we can replace each of the defining laws for well-behaved BXs by necessary conditions observed previously.
Theorem 4.1 (Characterizing well-behaved BXs). The following propositions are equiv-alent.
1. The GetPut and PutGetlaws hold.
2. The GetPut law holds, (‘put‘v) is idempotent for all views v , and “put s” is
injective for all sources s.
3. The PutGet law holds,(‘put‘v) is idempotent for all views v , and “uncurry put”
is surjective on the source type.
Proof. We show the implications 1⇒2⇒1⇒3⇒1.
1⇒2 The idempotence requirement follows from Proposition 3.8. The injectivity re-quirement is a direct consequence of thePutGetlaw (cf. Proposition 3.4).
2⇒1 To conclude thePutGet law
for all sourcess and viewsv, let pl be a left inverse of put (put s v). Then, verify the following equations using theGetPutlaw and Proposition 3.8.
get (put s v)
= { definition ofid }
id (get (put s v)) = { pl
is left inverse of put(put s v) }
pl
(put (put s v) (get (put s v))) = { GetPutlaw}
pl
(put s v)
= { idempotence of (‘put‘v), Proposition 3.8 }
pl
(put (put s v)v) = { pl
is left inverse of put(put s v) }
id v
= { definition ofid }
v
1⇒3 The idempotence requirement follows from Proposition 3.8. Surjectivity of “uncurry put” follows from Proposition 3.6.
3⇒1 To conclude the GetPut law, let pr be a right inverse of “uncurry put”, and
for a source s define “(s′,v) =pr
s” such that “put s′ v =s”. Then, verify the following equations using thePutGetlaw and Proposition 3.8.
put s (get s) = { put s′ v =s }
put(put s′ v) (get (put s′ v))
= { PutGetlaw}
put(put s′ v)v
= { idempotence of (‘put‘v), Proposition 3.8 }
put s′ v
= { put s′ v =s }
s
Theorem 4.2 (Uniqueness of get for well-behaved put). Assume a put function that satisfies all of the following propositions.
1. (‘put‘v) is idempotent for all views v .
2. “put s” is injective for all sources s.
3. “uncurry put” is surjective on the source type.
Then the following propositions are also satisfied.
(a) For every source s there is exactly one view v such that put s v =s.
(b) There is exactly one get function such that the resulting BX is well-behaved.
Proof. (a) Regarding the existence of v, choose for all s a sources′ and a viewv such
that s=put s′ v according to (3). Then, the following equations hold because of Proposition 3.8.
put s v
= { s=put s′ v }
put(put s′ v)v
= { idempotence of (‘put‘v), Proposition 3.8 }
put s′ v
= { s=put s′ v } s
A viewv satisfying the equationput s v =s is unique because “put s” is injective according to (2).
(b) Regarding the existence of get define
get s =v,with v such that s =put s v
according to (a). Then, we can verify theGetPutlaw as follows.
put s (get s)
= { definition ofget }
put s v,with v such that s =put s v
= { s=put s v }
s
From the second proposition of Theorem 4.1 we can now conclude that the resulting BX is well-behaved.
Regarding the uniqueness ofget, considerget′ such that the resulting BX is well-behaved. Then, we can observe the following equations making use of (a) and the
get′s
= { proposition (a)}
get′(put s v),with v such that s =put s v
= { PutGetlaw}
v,with v such that s =put s v
= { definition ofget }
get s
This result shows that well-behaved BXs are characterized by their putback function, i.e., theget function is redundant for the purpose of specification.
4.2 Characterizing very well-behaved BXs
Very well-behaved BXs differ from well-behaved BXs only in the PutPut law (see
Definition 2.4) which (as we have observed after Proposition 3.8) is a stronger version of the idempotence requirement on (‘put‘v) for all viewsv.
As a consequence, the following characterization of very well-behaved BXs is a direct consequence of Theorem 4.1.
Corollary 4.3 (Characterizing very well-behaved BXs). The following propositions are equivalent.
1. The GetPut, PutGet, and PutPut laws hold.
2. The GetPut and PutPutlaws hold and “put s” is injective for all sources s.
3. ThePutGetand PutPutlaws hold and “uncurry put” is surjective on the source
type.
Proof. Direct consequence of Theorem 4.1 because thePutPutlaw (cf. Proposition 3.1)
implies idempotence of (‘put‘v) for all views v.
We get a similar result regarding the uniqueness of the get function for a given put
function of a very well-behaved BX as we observed for well-behaved BXs.
Corollary 4.4 (Uniqueness of get for very well-behavedput). Assume a put function that satisfies all of the following propositions.
1. The PutPut law holds.
2. “put s” is injective for all sources s.
3. “uncurry put” is surjective on the source type.
Then there is exactly one get function such that the resulting BX is very well-behaved.
Proof. The propositions imply those of Theorem 4.2 so there is a unique get function such that the resulting BX is well-behaved. It is also very well-behaved because the put
4.3 Partial BXs
So far, we have assumed get and put to be functions —in the mathematical sense— between a source type S and a view type V. This entails, specifically, that get and put
are both total, i.e., yield a value for every argument in their respective domains. In the case of well-behaved BXs, totality ofget means surjectivity ofuncurry put and totality of put means surjectivity ofget.
While it is possible, in principle, to define precise types that match the domain and range of arbitrary get and put functions exactly, in practice, it is often convenient to allow the source and view types of bidirectional transformations be larger and defineget
orput as partial functions between these larger types [Pacheco, 2012].
Example 4.5 (Partial BX to access the head of a non-empty list). As an example for a partial bidirectional transformation, consider the following definitions.
getHead (x: ) =x putHead ( :xs)x =x:xs
In Haskell,(x :xs) denotes a list containing at least one element – x being the first and xs containing all remaining ones.
Here are some example calls, that demonstrate the behavior of the forward and backward functions using an alternative list notation.
getHead [1,2,3] = 1
getHead [ ] -- fails putHead [1,2] 3 = [3,2]
putHead [ ] 1 -- fails
If we define the source type for this transformation to be the type [Elem] of lists of elements of typeElem and the view type to be Elem then getHead andputHead do not form a well-behaved BX. The GetPut and PutGet laws are violated if we use the
empty list as a source value.
putHead [ ] (getHead [ ])6= [ ]
getHead (putHead [ ] 1) 6= 1
Also, note that one of the conditions on the put function used in Theorem 4.2 is violated: “uncurry putHead” is not surjective becauseput s v 6= [ ] for alls and v.
In Example 4.5, however, there is an easy way out. If we define the source type to be the type of non-empty lists thenputHead does satisfy all conditions of Theorem 4.2 and
Theorem 4.2 to derive a corresponding forward function automatically via the same reasoning we applied to Example 4.5.
Alternatively, we could reformulate our definitions such that get andput are partial functions and bidirectional laws are partial equalities. This relaxation still preserves all the above theorems (excluding surjectivity ofget and ofuncurry put) as long asget and
put are safe [Pacheco, 2012], in the sense that get is defined for the image of put and
put is defined for the image ofget. For space and readability reasons, we refrain from restating our results with partial functions.2
5 Put-based programming of BXs
Our main result, Theorem 4.2, states that in a well-behaved bidirectional transformation the definition ofget is redundant given a definition ofput that satisfies certain properties necessary for well-behavedness. In this section, we argue for specifying a well-behaved BX by defining aput function. We show how to use the functional-logic programming language Curry [Hanus (editor), 2012] to derive a correspondinggetfunction automatically and show, using several examples, how to define put functions for well-behaved BXs.
5.1 Using Curry to derive get from put
We can use the built-in search facilities of the functional-logic programming language Curry to derive theget function of a well-behaved bidirectional transformation from their
put function automatically. While search is probably not the most efficient way to obtain
get from put it is sufficient for the demonstration purposes of this section.
Syntactically, Curry is an extension of basic Haskell. Semantically, an important difference is the handling of pattern matching – especially in presence of multiple rules. In Curry, pattern-match failure is handled silently and more than one defining rule of a function (or more accurately: operation)3
may be applied nondeterministically. For example, the following program splits a given list in two parts at an arbitrary position.
split xs = ([ ],xs)
split (x:xs) = (x:ys,zs) where
(ys,zs) =split xs
The defining rules of split are overlapping but, unlike in Haskell, not only the first matching rule is applied but all matching rules are applied nondeterministically. For example, there are three possible results of the callsplit [1,2]:
([1,2],[ ]) ([1],[2]) ([ ],[1,2])
2
An Alloy [Jackson, 2012] model with precise partial definitions and a lightweight proof of Theorem 4.2
can be downloaded fromhttp://www.di.uminho.pt/~hpacheco/publications/Put.als.
3
Implementations of Curry usually allow to observe all nondeterministic results interactively and are free to present them in an arbitrary order.
An alternative way to definesplit is by constraining free variables. Instead of encoding nondeterminism using overlapping rules, we can also induce search by calculating with unknown information. Here is an alternative definition ofsplit following this approach.
split xs |xs=I ys++zs = (ys,zs) where
ys,zs free
This definition expresses in a guard that concatenating two unknown lists ys and zs
using the predefined operation “++” should yield the argument list xs. The Curry implementation searches for instantiations ofys andzs that satisfy the guard and returns them as result ofsplit. As there are, generally, multiple ways to instantiateys andzs to satisfy the guard, the result of split is nondeterministic like with the previous definition.4
In order to define the get function of a bidirectional transformation based on a put
function, we can use the same programming style as in the second definition ofsplit. For convenience, we first define a type for bidirectional transformations between a source type s and a view typev.
typeBX s v =s →v →s
The type BX s v defines bidirectional transformations as their put function. We provide a function put that just calls this function.
put::BX s v →s →v →s put bx s v =bx s v
The function get is defined based onput using the constraint given in Theorem 4.2.
get ::BX s v →s →v get bx s |put bx s v =I s =v
where
v free
These definitions allow todefine bidirectional transformations by giving only the putback function but touse them in both directions. In the remainder of this section we show several examples of defining and using bidirectional transformations in this putback style.
5.2 Record field access
The most basic bidirectional transformations access fields of records similarly to Exam-ple 1.1. To demonstrate record field access, we define a type for peoExam-ple.
4
dataPerson =Person Name City
dataName =Hugo |Sebastian |Zhenjiang
dataCity =Braga |Kiel |Tokyo
Example 5.1. We define bidirectional transformations name and city to access the name and associated city of a person, respectively.
name::BX Person Name
name (Person c)n =Person n c city::BX Person City
city (Person n )c=Person n c
Both definitions specify a bidirectional transformation by its putback function and we can issue calls in the Curry system KiCS2 to check that the derived forward function works as expected.
KiCS2i get name (Person Hugo Braga)
Hugo
KiCS2i get city(Person Zhenjiang Tokyo)
Tokyo
Of course, we can also call the putback function —directly or indirectly usingput— as the following examples demonstrate.
KiCS2i put city(Person Sebastian Tokyo)Kiel Person Sebastian Kiel
KiCS2i city (Person Sebastian Tokyo)Kiel Person Sebastian Kiel
We can also use these bidirectional transformations in other Curry functions. For example, the following predicate checks whether a person is from a given city.
isFrom::City →Person →Bool isFrom c p =c=I get city p
In the following, we define bidirectional transformations in analogy to database view updates using a database of people.
5.3 Database view updating
For the sake of simplicity, we regard database tables as sets of rows represented as lists sorted by a key identifying rows uniquely. For example, the following is a database of people where each person is identified by their name.
people = [hugo,sebastian,zhenjiang]
hugo =Person Hugo Braga sebastian =Person Sebastian Tokyo zhenjiang =Person Zhenjiang Tokyo
In order to update this database of people, the following function mergePeople will be helpful. It takes two tables of people (sorted by name) and merges them into a single (sorted) table of people. If entries with the same key are present in both tables then the
entry in the second table overwrites the entry in the first.
mergePeople:: [Person]→[Person]→[Person]
mergePeople old new =merge (sorted old) (sorted new) where
merge[ ]ps =ps
merge(p:ps) [ ] =p:ps merge(p:ps) (q:qs)
|get name p<get name q
=p:merge ps (q:qs)
|get name p=I get name q
=q:merge ps qs
|get name p>get name q
=q:merge (p:ps)qs sorted [ ] = [ ]
sorted (p:ps) =ascending p ps ascending p[ ] = [p]
ascending p(q:qs)
|get name p<get name q
=p:ascending q qs
The function mergePeople restricts the tables passed as arguments to be sorted using the partial function sorted that ensures that its argument is a sorted list of people. The functionsorted is the identity function on sorted tables but fails on lists of people that are not sorted by name (in mathematical terms, a coreflexive relation that is a subset of the identity relation).
Now, consider a database query that selects all people from a certain city. For example, selecting all people fromTokyo from thepeople database defined above would result in the following view of this database.
[Person Sebastian Tokyo,Person Zhenjiang Tokyo]
there is no person with that name in the original database then add it.5
For deletion, however, there is no straightforward update strategy. When deleting a person from the view, we can either
1. delete it from the original database or
2. change their city to a city different from Tokyo.
Keller [1986] argues that both strategies may be reasonable depending on context, so a system computing an update strategy automatically solely based on the definition of the view function is insufficient. Usingput-based bidirectional programming, both strategies above can be expressed in a straightforward way.
5.3.1 Reflecting deletions via deletions
The first strategy —deleting people from the original database that are not present in the updated view— can be implemented as follows:
• first, delete all people from the given city from the original database,
• then update the result by merging all people from the updated view.
Example 5.2 (Reflecting deletions via deletions). The following function peopleFrom implements a bidirectional transformation using the strategy described above.6
peopleFrom::City →BX [Person] [Person]
peopleFrom c source view =
letelsewhere =filter (not·isFrom c)source
in mergePeople elsewhere (map ensureCity view) where
ensureCity q |isFrom c q =q
The function peopleFrom uses mergePeople to merge the list elsewhere of people not from the given city in the originalsource with the list of people from the updatedview. The functionmergePeople ensures that both lists are sorted. Additionally, peopleFrom
restricts updated views using the local functionensureCity which is a partial identity function on people from the given city. Restricting updated views is important for maintaining the injectivity requirement of Theorem 4.2, as we discuss below. As a
5
In fact, these are not the only well-behaved ways to handle additions in a view. Changing the city of an existing person could be distinguished from deleting it and adding a new person if people
would have additional properties besides their name and city. Also, adding people not fromTokyo
would not violate well-behavedness if only performed when a person in the view is not present in the source. While our approach allows to define all such updates, we restrict ourselves to more reasonable strategies trying to keep updates minimal, which is consistent with update translation strategies used for database view updating.
6
consequence of this restriction, it is not possible to move people to a different city using this update strategy.
Conceptually,peopleFrom c is a bidirectional transformation between the source type of sorted lists of people and the view type of sorted lists of people from the cityc. Note that specifying the view type in the type system would require a dependently typed programming language, i.e., one where the types of expressions can depend on the values of others. Curry is not dependently typed, so we definepeopleFrom cas a partial function instead.
To verify that the get-function derived by our framework is unique and the resulting transformation is well-behaved, we need to check the following three conditions:
1. peopleFrom c (peopleFrom c s v)v =peopleFrom c s v for all citiesc, sorted lists
s of people, and sorted lists v of people from the city c,
2. peopleFrom c s is injective for all citiesc and sorted lists of people s, and
3. uncurry (peopleFrom c) is surjective on sorted lists of people for all citiesc.
The first condition is satisfied because the second application ofpeopleFrom c will remove the updated people and then re-add them, so updating twice using the same view is the same as updating only once.
The second condition is satisfied because peopleFrom c restricts updated views to people from the given city and is not defined for other views. Without this restriction, views that contain people from the original database not from the cityc would map to the same updated source as views not containing them, violating the injectivity requirement. By deleting all people from the city c from the original source and ensuring that people in the updated view are from the city c,peopleFrom c ensures that updated views are mapped uniquely to updated sources.
The third requirement is satisfied because every database of people can be obtained usingpeopleFrom c by passing it as original source together with a view that includes all its people from the city c.7
Together, these conditions ensure that the get function derived forpeopleFrom c is unique and the resulting BX is well-behaved. The following calls demonstrate the behavior of the derived view function and the defined update strategy.
KiCS2i get (peopleFrom Tokyo)people
[Person Sebastian Tokyo,Person Zhenjiang Tokyo]
KiCS2i put(peopleFrom Tokyo)people [zhenjiang] [Person Hugo Braga,Person Zhenjiang Tokyo]
KiCS2i put(peopleFrom Tokyo)people [put city hugo Tokyo,zhenjiang] [Person Hugo Tokyo,Person Zhenjiang Tokyo]
7
The first call demonstrates the get function querying all people from Tokyo in the database defined earlier. The second call demonstrates deleting sebastian by deleting him from the updated view passed to the put function. The result contains hugo who is not fromTokyo and zhenjiang who was included in the updated view. The third call demonstrates deleting sebastian and moving hugo to Tokyo by adding him to the list of people fromTokyo.
5.3.2 Reflecting deletions via modifications
Instead of deleting people from the database that are not present in the updated view queried by city we can also move them to a different city. This strategy can be implemented as follows:
1. first move all people from the queried city to the new city in the original source,
2. then call the update strategy defined in Section 5.3.1 to overwrite all moved people who are present in the view, effectively moving only those who are not present.
Example 5.3 (Reflecting deletions via modifications). The following definition imple-ments the strategy described above.
peopleFromTo::City →City →BX [Person] [Person]
peopleFromTo from to source view = letmoved =map move source
in peopleFrom from moved view
where
move p |get city p=I from =put city p to
|otherwise =p
Again, we need to verify the conditions of Theorem 4.2 to ensure that the resulting BX is well-behaved:
1. Putting an original source with the same view twice is the same as updating it only once because the underlying transformation peopleFrom satisfies this property for all sources, i.e., also for the modified source passed bypeopleFromTo.
2. The injectivity requirement is also implied by the corresponding property for the underlying transformation.
3. Regarding surjectivity, note that, even though people in the original source are moved initially, they can be moved back by including all moved people in theview
argument. So obtaining an arbitrary source as result ofpeopleFromTo is achieved in the same way as forpeopleFrom.
KiCS2i get (peopleFromTo Tokyo Kiel)people
[Person Sebastian Tokyo,Person Zhenjiang Tokyo]
KiCS2i put(peopleFromTo Tokyo Kiel)people [zhenjiang]
[Person Hugo Braga,Person Sebastian Kiel,Person Zhenjiang Tokyo]
KiCS2i put(peopleFromTo Tokyo Kiel)people [put city hugo Tokyo,zhenjiang] [Person Hugo Tokyo,Person Sebastian Kiel,Person Zhenjiang Tokyo]
The get function of the BX peopleFromTo Tokyo Kiel is the same as the get function of peopleFrom Tokyo. The difference is only in the put function which moves sebastian
fromTokyo to Kiel when he is deleted from theview instead of deleting him from the
source. Inserted people, like hugo, are inserted into the original source (or modified if they already exist) just like before.
5.3.3 Missing support for ensuring well-behavedness
Examples 5.1 through 5.3 show how to write bidirectional transformations in putback style. The definitions inspired by database queries follow a verbal description of update strategies and are implemented modularly by reusing common parts. We have argued informally that our definitions satisfy the necessary conditions for the transformations to be well-behaved and observed their behavior using example calls.
Ensuring well-behavedness can be tricky, however. As an example of a bidirectional transformation where well-behavedness is possible but not easily ensured, we discuss joins of database tables without showing their implementation.
Consider that we define datatypes for books associating titles with owners which allow the following definitions.
someBooks = [Book The Art of Computer Programming Zhenjiang,
Book The Elements of Style Sebastian,
Book The Lord of the Rings Hugo]
somePeople = [hugo,zhenjiang]
The result of joining the tables someBooks andsomePeople is the following list of pairs containing titles and cities.
[(The Art of Computer Programming,Zhenjiang,Tokyo),
(The Lord of the Rings,Hugo,Braga)]
Sebastian’s book is not included because he is not listed in the table somePeople. Say, we want to update this join to include another book owned by Sebastian and at the same time removeHugo’s book.
someJoin = [(The Art of Computer Programming,Zhenjiang,Tokyo),
(To Mock a Mockingbird,Sebastian,Tokyo)]
1. Should books likeThe Element of Style that are not part of the updated view be included in the book table of the updated source?
2. What about the explicitly removed bookThe Lord of the Rings?
3. Can we always add such new books to the book table?
4. Can we always add new owners to the person table?
We will answer these questions in turn considering well-behavedness of the resulting transformation.
1. Books like The Elements of Style that are not part of the view but of the book table in the original source need to be included in order to satisfy theGetPutlaw.
If we do not include such books in the updated book table, we could not update the source (someBooks,somePeople) with it’s join and get back the same source. On the other hand, we need to delete such books from the updated source, if the view is updated with other books of the same owner for reasons discussed below.
2. For deleted books likeHugo’s we have different options. We can delete the book from the updated book table or delete the owner from the updated person table. When deleting a book from the book table, we need to distinguish this case from the previous case where we have to keep a book that is not part of the view because the owner is not in the person table. DeletingHugo from the people table is admissible in this case because he has no other books. If there were other books owned by
Hugo in the original book table, however, we could not delete him from the updated people table without violating the PutGetlaw: when computing the join for the
updated source, all other books owned byHugo would be missing.
3. We can (and, because of the PutGetlaw, have to) add new books to the book
table.
4. We can add new owners to the person table if they do not have other books listed in the book table but need to be careful about adding owners of other books. For example, if we add Sebastian to the updated person table because his bookTo Mock a Mockingbird should be included in the view, his other book
The Elements of Style would also be included. Hence, we need to delete all other books from newly added owners or disallow adding books from new owners.
6 Related Work
The literature most related to our theory of BXs can be classified according to two main categories.
The first focuses on taking an existing language for defining theget function, and then trying to derive a suitable put function through bidirectionalization techniques. This kind of bidirectional approach has been mostly followed in the database community, where it is known as the classical view-update problem. A database administrator may define views that provide simplified or restructured information to users. Since the view typically contains less information than the source, a view update can be translated in general into multiple source updates, and the problem lies in how to choose a suitable update translation strategy.
The second approach is to design a bidirectional programming language in which a programmer writes both the get function and the put function in a single expression. Bidirectional programming languages for the kinds of BXs considered in this paper, where the get function defines a view and the backward function a view update strategy, are usually calledlenses.
Deeper and broader revisions of related work on bidirectional transformations can be found in [Foster, 2009, Pacheco, 2012, Czarnecki et al., 2009, Hu et al., 2011].
6.1 View-update Problem
Work on database view-update translation has a long tradition in the database community, going back to the late 70s and 80s when it was extensively studied.
In seminal work, Bancilhon and Spyratos [1981] remark that, given a complement function such that the tupled get-complement function is injective, the translation of view updates under a constant complement is unique. Their formulation is essentially isomorphic to very well-behaved BXs [Foster et al., 2007].
To formalize the notion of a reasonable complement, Hegner [2004] extends the closed views theory of Bancilhon and Spyratos [1981] with a notion of order on source and view updates, such thatput is monotonic: the reflection of an insertion in the view is an insertion in the source, and similarly for deletions. He then establishes that for a
get written in a monotonic SPJ (select-project-join) relational algebra, there is a unique translation of insertion and deletion view updates independently of the choice of the complement.
Although closed views guarantee that view updates do not affect parts of the database that are not visible through the view, they are often too conservative and disallow many reasonable view update translations that do not keep any complement constant. A more liberal theory of open views that rejects fewer updates but permits several reasonable translations is proposed by Dayal and Bernstein [1982]. They formalize that a correct view update translation shall simply not introduce view side effects, and propose algorithms that perform one possible update translation for views written in a SPJ relational algebra. Their formulation is essentially isomorphic to well-behaved BXs [Foster et al., 2007].
effects in the source database that users are not aware of by only looking at the view. Since different translations may be more appropriate for different scenarios, Keller [1986] proposes an interactive algorithm that, based on a SPJ view definition, runs a dialog with the view programmer to choose a particular view update policy that obeys a set of intuitive criteria.
Other authors like Larson and Sheth [1991] point out that, for some examples, the available information at view definition time is not sufficient for a view programmer to unambiguously select a suitable view update strategy, and that information about the issued view update is necessary. Using similar criteria as Keller [1986], they propose an interactive algorithm that collects semantic information both at view definition time (provided by the view programmer) and at view update time (provided by the view user), and permits choosing from a larger number update policies for a broader class of view definitions written using also relational difference, union and intersection.
A common feature of these relational BX approaches is that they are operation-based, i.e., they consider actual edit operations in contrast to our state-based BXs that consider whole source and view states, and the proposed update strategies process insertion, deletion and modification updates independently. For example, an update strategy that reacts to block operations like deleting a group in the source if all members of the group are deleted in the view is not definable in an approach that considers independent view updates. Moreover, the approaches with dialog only consider update translators that satisfy a given set of criteria deemed intuitive (normally by trying to reduce the number of source side effects), but not all well-behaved update translators. For example, the lens from Example 2.3 would be typically left out. Note also thatput programming is not a commitment to an update translator at putback definition time: the view programmer can leave parameters (that do not affect the derivedget function) to be controlled by users at view update time.
6.2 Bidirectional Programming Languages
In the last ten years, various bidirectional programing languages have become increasingly popular across a wide range of communities, including data synchronization, model transformations, graph transformations, relational databases and functional programming. We review only a few that are more related to our work.
The pioneering work of Foster et al. [2007] proposes one of the first bidirectional programming languages for defining views of tree-structured data. They recast many of the ideas for database view-updating into the design of a language of BXs named lenses, consisting of aget and aput function that satisfy well-behavedness laws analogous to the ones proposed by Dayal and Bernstein [1982] and Bancilhon and Spyratos [1981]. The novelty of their work is by putting emphasis on types and totality of lens transformations, and by proposing a series of combinators that allow reasoning about totality and well-behavedness of lenses in a compositional way. The kinds of BXs studied in our paper are precisely total (very) well-behaved lenses.
provide one possible update policy based on a careful treatment of functional dependencies. They also develop a type system using record predicates and functional dependencies to express the exact conditions on the source and view schemas under which lenses are total and well-behaved.
Bohannon et al. [2008] design a language for the bidirectional transformation of string data, built using a set of regular operations and a type system of regular expressions. To overcome issues with order, their lens combinators adopt an update translation strategy based on keys that are introduced by the programmer in the form of annotations to lens expressions. Matching lenses [Barbosa et al., 2010] generalize the string lens language by lifting the update translation strategy from a key-based matching to support a set of different alignment heuristics that can be chosen by users.
Pacheco and Cunha [2010] propose a point-free functional language of total well-behaved lenses, using a simple positional update strategy, and later Pacheco et al. [2012] extend the matching lenses approach to infer and propagate insertion and deletion updates over arbitrary views defined in such point-free language.
Hidaka et al. [2010] propose the first linguistic approach for bidirectional graph trans-formations, by giving a bidirectional semantics to the UnCal graph algebra. Although their base semantics is compositional, they process deletions in the view by locating the correlated subgraph in the source, and for insertions in the view they have a dialog with the user at view update time to calculate the correlated inserted subgraph in the source.
All existing bidirectional programing approaches based on lenses focus on writing bidirectional programs that resemble writing theget function, and possibly take some additional parameters that provide limited control over the update strategy of the put
function. Since these languages are state-based, theput function of a lens must align the updated view and the original source structures to identify the modifications and translate them to the source accordingly. Although for unordered data (relations, graphs) such alignment can be done rather straightforwardly, for ordered data (strings, trees) it is more problematic to find a reasonable alignment strategy, and thus to provide a reasonable view update translation strategy. Our results open the way to put programming languages, that in theory could give the programmer the possibility to express all well-behaved update translation strategies.
In his PhD thesis, Foster [2009] independently discusses a characterization of lenses in terms ofput functions (considering only totalget andput functions), in point-wise terms, similar to our main theorem. Interestingly, he arrives at a notion of put semi-injectivity
that is slightly stronger than our injectivity ofput s. He also uses thePutTwice law
which we identify as idempotence of ‘put‘v. Nevertheless, he does so only to plead for a forward programming style and does not pursue a putback programming style. Moreover, he advocates that both styles are equivalent because writing a bidirectional program in a
for the backward update strategy to specify a BX completely. We explore the putback style to demonstrate this difference and illustrate a possible way to derive get functions from put functions.
6.2.1 Symmetric Bidirectional Programming Languages
Bidirectional programming languages in the style of lenses areasymmetric, in the sense that get is surjective and the view type usually contains less information than the source type. In asymmetric bidirectional programming language, both the source and target types may contain information not present on the other side, giving rise to different laws and mathematical properties.
Meertens [1998] studies the construction of a language of constraint maintainers for preserving the consistency of artifacts in user interfaces. A maintainer has a forward functionget :: (S,T) →T that propagates source updates, a backward function put:: (T,S)→S that propagates target updates and a consistency relation R⊆(S, T) that the functions must preserve. Meertens [1998] also notes that composition of maintainers is not well-behaved in general, but interestingly proves that the composition of two well-behaved lenses with a common view type yields a well-behaved maintainer between their source types.
Hofmann et al. [2011] build a language of symmetric lenses over algebraic data structures. A maintainer consists of two transformations get :: (S,C) → (T,C) and
put:: (T,C)→ (S,C) and a complement c::C that preserves a history of the source and target information lost through previous update translations. Unlike maintainers, symmetric lenses support composition. They also show that any symmetric lens can be viewed as the composition of two lenses with a common source consisting of the domain of consistent triples of type (S,C,T).
7 Conclusions and Future Work
In this article, we characterize the class of (very) well-behaved bidirectional transforma-tions solely based on their putback functransforma-tions. In doing so, we rephrase existing laws for BXs based on simple mathematical concepts such as injectivity, surjectivity, and idempotence. We use our characterization to show that (very) well behaved BXs are uniquely determined by their backward functions and corresponding forward functions can be obtained automatically. In sharp contrast to bidirectional programming approaches based onget, writing put is sufficient to express all (very) well-behaved BXs.
The first immediate direction for future work is to investigate the design ofput program-ming languages for particular data domains, that guide users by only allowing them to define well-behaved BXs but retain the full power of writing put. Notwithstanding, users are not necessarily obliged to fully control the update strategy: as for get programming, default parameters for put may be used when adequate. In fact, we believe that a style of injectiveput s functions with clear inverses can prove to be equally manageable and even more intuitive than the traditional style of surjective get functions with ambiguous inverses. Moreover, a fully expressiveput programming language for a particular data domain (e.g., databases and relational algebra) could serve as a unified framework to express and compare BX approaches in that domain; and interfaces for existing BX approaches could be implemented on top of the core framework. Such a unified framework would constitute a foundational response to the recently growing unification effort of the different BX communities, stated in publications such as [Czarnecki et al., 2009, Hu et al., 2011, Terwilliger et al., 2012].
Some bidirectional programming approaches [Keller, 1986, Larson and Sheth, 1991, Hidaka et al., 2010] relax the requirement imposed byPutGetto admit view side effects
in some particular cases, instead of disallowing view updates. An interesting direction for future work would be to investigate how to extend our theory to consider view side effects. Another challenging direction is to discover how to uniquely specify classes of symmetric BXs, either directly or by decomposing them into pairs of asymmetric BXs.
Acknowledgments
We thank Keisuke Nakano who inspired an example we use to show the ambiguitiy in specifying bidirectional transformations using only the forward function.
References
F. Bancilhon and N. Spyratos. Update semantics of relational views. ACM Transactions on Database Systems, 6(4):557–575, 1981.
D. M. J. Barbosa, J. Cretin, J. N. Foster, M. Greenberg, and B. C. Pierce. Matching lenses: alignment and view update. InProceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), pages 193–204. ACM, 2010.
A. Bohannon, B. C. Pierce, and J. A. Vaughan. Relational lenses: a language for updatable views. InProceedings of the 25th ACM SIGMOD Symposium on Principles of Database Systems (PODS 2006), pages 338–347. ACM, 2006.
